es:ES, i, x, y:Id, A, B:Type, I:(AB).
@i(x:A)
 @i(y:B)
 e@i. (first(e))  I(x when e,y when e)
 e@i. I(x when e,y when e)  I((x after e),(y after e))
 @i always.I(x,y) 

latex

Definitions	True, T, A c B, x. t(x), t  T, P & Q, @i always.P(x1;x2), x(s1,s2), e@i. P(e), P  Q, , x:A. B(x), {T}, SQType(T), P  Q, x(s), P  Q, @i(x:T)
Lemmas	event system wf, es-dtype wf, Id wf, alle-at wf, es-loc wf, es-first wf, assert wf, not wf, es-pred wf, true wf, squash wf, subtype rel wf, es-after wf, es-loc-pred, Id sq, es-after-pred, es-vartype wf, es-when wf, alle-at-iff